package trabajoISW2.domain.contracts;

import java.util.Calendar;

import tdg.contract.semanticAnnotations.Inv;
import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Query;
import trabajoISW2.domain.implementations.Address;
import trabajoISW2.domain.implementations.Cart;
import trabajoISW2.domain.implementations.CreditCard;

@Inv("getCartId().compare(null) != 0")
public interface IOrder {

	@Query
	public int getOrderId();
	
	@Pre({"id >= 0 && id <= Integer.MAX_VALUE #WrongIdException"})
	@Pos("getOrderId() == Id")
	public void setOrderId(int id);
	
	@Query
	public Calendar getDate();
	
	

	@Pre("c !=null #IllegalArgumentException")
	@Pos({"getCreditCardNumber().equals(c)"})
	public void setCreditCard(CreditCard c);

	@Query
	public CreditCard getCreditCard();
	
	@Pre("ad !=null #IllegalArgumentException")
	@Pos({"getAddress().equals(ad)"})
	public void setAddress (Address ad);

	@Query
	public Address getAddress();
	
	@Query
	public Cart getCart();
	
	@Pre("cart !=null #IllegalArgumentException")
	@Pos({"getCart().equals(cart)"})
	public void setCart(Cart cart);
	
	@Query
	public void showInvoice();
}
